Process Analysis Toolkit  (PAT) 3.5 Help  
3.8.1.2 Addon for Verification.htm

Sites for Verification

Global Variable

As Orc does not have a notion of global variable, in order to be able to easily assert a global property that holds throughout the program, we extend Orc with a notion of global variable. Global variable in Orc must prefixed by globalvar keyword, and defining at the beginning of the program.

GUpdate Site 

To assign a value to a global variable directly, a special site $GUpdate is provided.

Consider the metronome example in Section 3.8.1.1 with global variables and $GUpdate inserted, 

globalvar tickNum = 0
      metronome(1000) >> $GUpdate({tickNum = tickNum + 1})>> "tick"
    | Rtimer(500) >> metronome(1000) >> $GUpdate({tickNum = tickNum - 1}) >> "tock"

we can verify whether it is possible to have two consecutive "tick"s or two consecutive "tock"s by checking whether the system is able to reach the state satisfying (tickNum < 0 \/ tickNum > 1).

Global Variable InitializationSometimes, global variable need to be initialized before its use.  The intialization section is declared just after the global variable declaration, and the section is surrounded by curly bracket { }.

Consider the example below, the global variable arr is a two-element array, and it is initialize with the value [2,1] before it is passed the the quicksort function.

globalvar arr=Array(2)
     {arr.set(0,2)>>arr.set(1,1)}
      def quicksort{a}= ...
      quicksort(arr)

External Sites Modeling

Service orchestration systems would normally involve external services. External services would incur, furthermore, there might be cases where communication halted unexpectedly, or the services simply non-responsive.

Following is the syntax that used to model the external site,

ExternalSite SiteName(Args)[haltAllow{Delay}]{DelayTups}
      SystemVarDecls
      {SystemVarInits}
      ORCExpression
 EndSite

where ExternalSite and EndSite denotes the start and end of the external site modeling. SiteName is the service name of the external site; Args is a set of arguments for the site; haltAllow is an optional tag to specify whether to model the halting behavior, and Delays is a set of natural numbers which denotes the possible delays before halting. DelayTups is a set of tuple (t1,t2) which is used to specify all possible communication delays of the external service. The domain of t1 and t2 is natural numbers. t1 is the forward trip delay, which is used to specify the communication delay for the service call to reach the external services plus the processing time needed just before the internal storage of external services is updated. For simplicity of modeling, internal storage of external services are assumed to be updated instantaneously at time t1 and if there are multiple internal storages to be updated, we assumed all are updated at the same time. t2 is the return trip delay, which is used to specify the processing time of the external services just after the update of internal storage plus the delay of returned value traveling back from the external service. Thus, the total roundtrip delay is t1 + t2. DelayTups also allows a special "inf "(infinity delay) symbol, which is used to denote the non-responsive behavior. SystemVarDecl is a list of system variable declarations, which is used to model the global internal storage for the stateful external service. All the system variable declarations are required to start with the systemvar keyword. SystemVarInits is the section that initialize the declared system variables, and the section is surrounded by curly bracket {} just like global variable intialization.ORCExpression is the body of the external site modelling and it is used to specify the output value of external site with respect to the input arguments Args.

Example - Auction Service

ExternalSite Auction(x)[haltAllow{1, 2}]{(1,1), inf} =
    systemvar AuctionList = Buffer()
    {AuctionList.put("1")}
    (x > ("post", item) > AuctionList.put(item)
    |
    x > "getNext" > AuctionList.getnb()
EndSite

The above syntax specifies an Auction external site. AuctionList is started with a value "1".
Assume argument x=("post", 100), the possible behaviors are

  • A. After 1 time unit, the external services updated the Auction-List with the value 100, and spent another 1 time unit for the signal value to come back to the caller;
  • B. After 1 time unit, the system is halted;
  • C. After 2 time units, the system is halted;
  • D. The service call is non-responsive.

 
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.